//package formula;
//
//import sign.FormulaSign;
//
//import java.util.Objects;
//import java.util.function.ToDoubleBiFunction;
//
//public class TripleFormula extends Formula{
//    FormulaSign sign;
//    UnaryFormula left;
//    BinaryFormula right;
//
//    public TripleFormula(FormulaSign sign,UnaryFormula left,BinaryFormula right){
//        this.sign=sign;
//        this.left=left;
//        this.right=right;
//    }
//
//    @Override
//    public String toString(){
//        return sign + "(" + left + "," + right + ")";
//    }
//
//    public FormulaSign getSign(){
//        return sign;
//    }
//    public Formula getLeft(){
//        return left;
//    }
//    public Formula getRight(){
//        return right;
//    }
//
//    //重写equals方法
//    //TODO
//    @Override
//    public boolean equals(Object o) {
//        if (this == o) return true;
//        if (o == null || getClass() != o.getClass()) return false;
//        TripleFormula that = (TripleFormula) o;
//        return toString().equals(that.toString());
//    }
//
//    //实现TF的取反
//    public TripleFormula getNegated(){
//        if (this.getSign()==FormulaSign.ANY){//对 any(p1,exist(pn,r))取反
//            //结果为 exist(p1,any(pn,not r))
//            BinaryFormula tf_right=(BinaryFormula) this.getRight();
//            UnaryFormula bf_right=(UnaryFormula) tf_right.getRight();
//            UnaryFormula negatedUF=bf_right.getNegated();
//            BinaryFormula newBF=new BinaryFormula(FormulaSign.ANY, ((BinaryFormula) this.getRight()).getLeft(),negatedUF);
//            TripleFormula result=new TripleFormula(FormulaSign.EXIST,(UnaryFormula) this.getLeft(),newBF);
//            return result;
//        }else if (this.getSign()==FormulaSign.EXIST){//对 exist(p1,any(pn,not r))取反
//            //结果为 any(p1,exist(pn,r))
//            BinaryFormula tf_right=(BinaryFormula) this.getRight();
//            UnaryFormula bf_right=(UnaryFormula) tf_right.getRight();
//            UnaryFormula negatedUF=bf_right.getNegated();//r
//            BinaryFormula newBF=new BinaryFormula(FormulaSign.EXIST, ((BinaryFormula) this.getRight()).getLeft(),negatedUF);
//            TripleFormula result=new TripleFormula(FormulaSign.ANY,(UnaryFormula) this.getLeft(),newBF);
//            return result;
//
//        }else {return null;}
//    }
//
//    //判断两个TF是不是互斥的
//    public boolean isNegated(TripleFormula tf){
//        TripleFormula transition=tf.getNegated();
//        if (this.equals(transition)){
//            return true;
//        }else {return false;}
//    }
//
//}
